COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	!fcnappend&3 u*v ← qif qn u qthen v qelse qa u . [qd u * v].
C00004 00003	The Samefringe problem
C00006 00004	 PARTN TOP DOWN
C00008 ENDMK
C⊗;
!fcnappend&3 ⊗⊗⊗u*v ← qif qn u qthen v qelse qa u . [qd u * v]⊗.
!fcnomega& ⊗⊗⊗omega x ← omega x . $$A$⊗.
!fcnappend&4 ⊗⊗⊗u*v ← qif qn u qthen v qelse qa u . [qd u * v]⊗.

!fcnsize&2 ⊗⊗⊗size x ← qif qat x qthen $1 qelse size qa x + size qd x⊗,

!fcnfringe&3 ⊗⊗⊗fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x⊗,

!fcnltngth&h3 ⊗⊗⊗length u ← qif qn u qthen $0 qelse $$1$ + length qd u⊗


⊗⊗⊗flatten[x] ← flat[x, qNIL]		⊗
!fcnflatten&3 
⊗⊗⊗flat[x,u] ← qif qat x qthen x.u qelse flat[qa x,flat[qd x,u]]⊗.
!fcnlose&  ⊗⊗⊗lose x ← ¬lose x ⊗.
!fcnsubexpf& ⊗⊗⊗subexpf[x, y] ← [x = y] ∨ [¬qat y ∧ [subexpf[x, qa y] ∨ subexpf[x, qd y]]]⊗.
!fcnsamefringe&  ⊗⊗⊗samefringe[x, y] ← x = y ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]⊗

!fcnsame&  ⊗⊗⊗same[x, y] ← qa x = qa y ∧ samefringe[qd x, qd y]⊗

!fcngopher&  ⊗⊗⊗gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗.
∂(n)⊗⊗samefringe[x, y] ← ⊗
∂(n)⊗⊗    x = y ∨ ⊗
∂(n)⊗⊗    [¬qat x ∧ ¬qat y ∧ ⊗
!fcnsamefringe&1  ∂(n)⊗⊗        [qif qat qa x qthen [qif qat qa y qthen qa x = qa y ∧ samefringe[qd x, qd y] ⊗
∂(n)⊗⊗                             qelse samefringe[x, qaa y. [qda y . qd y]]]⊗
∂(n)⊗⊗         qelse samefringe[qaa x . [qda x . qd x], y]. ⊗
;;;The Samefringe problem

(DEFUN SAMEFR (X Y)
  (OR (EQ X Y) (AND (NOT (ATOM X)) (NOT (ATOM Y)) (SAME (GOPHER X) (GOPHER Y)))))

(DEFUN SAME (X Y) (AND (EQ (CAR X) (CAR Y)) (SAMEFR (CDR X) (CDR Y))))

(DEFUN GOPHER (X)
  (COND ((ATOM (CAR X)) X)
	(T (GOPHER (CONS (CAAR X) (CONS (CDAR X) (CDR X))))) ))

(DEFUN SAMEFR# (X Y) 
  (OR (EQ X Y) 
      (AND (NOT (ATOM X)) (NOT (ATOM Y)) (SAME3 (CAR X) (CDR X) (CAR Y) (CDR Y))) ))

(DEFUN SAME3 (XA XD YA YD)
  (COND ((ATOM XA) 
	  (COND ((ATOM YA) (AND (EQ XA YA) (SAMEFR3 XD YD)))
		(T (SAME3 XA XD (CAR YA) (CONS (CDR YA) YD)))))
	((ATOM YA) (SAME3 (CAR XA) (CONS (CDR XA) XD) YA YD))
	(T (SAME3 (CAR XA) (CONS (CDR XA) XD) (CAR YA) (CONS (CDR YA) YD)))))
	

(DEFUN SAMEFRINGE (X Y)
  (OR (EQUAL X Y) 
      (AND (NOT (ATOM X)) (NOT (ATOM Y)) 
	   (COND ((ATOM (CAR X)) 
		  (COND ((ATOM (CAR Y)) 
		         (AND (EQUAL (CAR X) (CAR Y)) (SAMEFRINGE (CDR X) (CDR Y))) )
			(T (SAMEFRINGE X (CONS (CAAR Y) (CONS (CDAR Y) (CDR Y))))) ))
	   	 (T (SAMEFRINGE (CONS (CAAR X) (CONS (CDAR X) (CDR X))) Y)) ))) )



;;; PARTN TOP DOWN

(DEFUN LISTP (X)
  (OR (NULL X) (LISTP (CDR X))) )

(DEFUN NELIST (X)
  (AND (LISTP X) (NOT (NULL X))) )

(DEFUN UULIST (X)
  (OR (NULL X) (AND (NELIST (CAR X)) (UULIST (CDR X)))) )

(DEFUN ISPARTN (W U N)
  (AND (UULIST W) (EQUAL (LENGTH W) N) (EQUAL (COMBINE W) U)) )


(DEFUN TACK0 (X PPL)
  (COND ((NULL PPL) NIL)
	(T (CONS (CONS (CONS X (CAAR PPL)) (CDAR PPL))
		 (TACK0 X (CDR PPL))) )) )

(DEFUN TACK1 (UU PL)
  (COND ((NULL PL) NIL)
	(T (CONS (CONS UU (CAR PL))
		 (TACK1 UU (CDR PL))) )) )

(DEFUN COMBINE (UL)
  (COND ((NULL UL) NIL)
	(T (APPEND (CAR UL) (COMBINE (CDR UL)))) ))

(DEFUN PARTN (U N)
  (COND ((NULL U) (COND ((EQUAL N 0) (LIST NIL)) (T NIL)))
	((EQUAL N 0) NIL)
	(T (APPEND (TACK1 (LIST (CAR U)) (PARTN (CDR U) (SUB1 N)))
                   (TACK0 (CAR U) (PARTN (CDR U) N)))) ))